The main challenge in using abstractions effectively, is to construct asuitable abstraction for the system being verified. One approach that tries toaddress this problem is that of {\it counterexample guidedabstraction-refinement (CEGAR)}, wherein one starts with a coarse abstractionof the system, and progressively refines it, based on invalid counterexamplesseen in prior model checking runs, until either an abstraction proves thecorrectness of the system or a valid counterexample is generated. While CEGARhas been successfully used in verifying non-probabilistic systemsautomatically, CEGAR has not been applied in the context of probabilisticsystems. The main issues that need to be tackled in order to extend theapproach to probabilistic systems is a suitable notion of ``counterexample'',algorithms to generate counterexamples, check their validity, and thenautomatically refine an abstraction based on an invalid counterexample. In thispaper, we address these issues, and present a CEGAR framework for MarkovDecision Processes.
展开▼
